『Homotopy type theory and Voevodsky's univalent foundations』
Álvaro Pelayo, Michael A. Warren, Homotopy type theory and Voevodsky's univalent foundations, 2012
code:memo
Abstract. Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened “homotopy type theory”. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky’s setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky’s work using the well-known proof assistant Coq. The paper is written for a generalaudience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science.
概要 最近、抽象的なホモトピー理論と、論理学や理論計算機科学の型理論の分野を結びつける発見がなされた。これにより、「ホモトピー型理論」と命名された新分野が誕生した。ウラジーミル・ヴォエヴォドスキーは、単体的集合を用いた型理論のモデル化が可能であることを発見し、このモデルが「一価性の公理」と呼ばれる付加的性質を満足することを明らかにした。彼はその後、ユニヴァレント・ファウンデーションと呼ぶプログラムを提唱し、一価性の公理と、場合によっては単体的集合モデルに動機づけられた他の公理を備えた型理論の設定で数学を発展させることを提唱した。型理論は優れた計算特性を持つので、このプログラムはコンピュータの証明アシスタントの中で実行することが可能である。本論文では、ヴォエヴォドスキーの設定におけるホモトピー型理論について、理論的および実用的な問題に注意を払いながら紹介する。特に、この論文は、ホモトピー型理論の一般的な考え方と、よく知られた証明支援系Coqを使ったヴォエヴォドスキーの仕事の具体的な詳細の両方への導入として機能するものです。本論文は、代数的位相幾何学の基礎知識を持つ数学者の一般読者を対象としており、型理論、論理学、コンピュータサイエンスの予備知識は一切想定していない。
www.DeepL.com/Translator（無料版）で翻訳しました。